WORST_CASE(?,O(n^2)) Solution: --------- "!EQ" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(13, 14) "0" :: [] -(0)-> "A"(0, 0) "Cons" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) "Cons" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "Cons" :: ["A"(0, 0) x "A"(11, 11)] -(0)-> "A"(0, 11) "Cons" :: ["A"(4, 0) x "A"(10, 6)] -(4)-> "A"(4, 6) "Cons" :: ["A"(3, 0) x "A"(14, 11)] -(3)-> "A"(3, 11) "Cons" :: ["A"(11, 0) x "A"(15, 4)] -(11)-> "A"(11, 4) "Cons" :: ["A"(4, 0) x "A"(4, 0)] -(4)-> "A"(4, 0) "Cons" :: ["A"(0, 0) x "A"(6, 6)] -(0)-> "A"(0, 6) "Cons" :: ["A"(0, 0) x "A"(8, 8)] -(0)-> "A"(0, 8) "False" :: [] -(0)-> "A"(0, 0) "False" :: [] -(0)-> "A"(7, 10) "False" :: [] -(0)-> "A"(13, 14) "False" :: [] -(0)-> "A"(13, 15) "False" :: [] -(0)-> "A"(6, 0) "False" :: [] -(0)-> "A"(6, 1) "False" :: [] -(0)-> "A"(4, 0) "False" :: [] -(0)-> "A"(14, 14) "False" :: [] -(0)-> "A"(6, 4) "Nil" :: [] -(0)-> "A"(4, 6) "Nil" :: [] -(0)-> "A"(0, 11) "Nil" :: [] -(0)-> "A"(1, 0) "Nil" :: [] -(0)-> "A"(0, 0) "Nil" :: [] -(0)-> "A"(11, 4) "Nil" :: [] -(0)-> "A"(3, 11) "Nil" :: [] -(0)-> "A"(4, 0) "Nil" :: [] -(0)-> "A"(14, 10) "Nil" :: [] -(0)-> "A"(14, 15) "Nil" :: [] -(0)-> "A"(14, 14) "Nil" :: [] -(0)-> "A"(15, 14) "S" :: ["A"(0, 0)] -(0)-> "A"(0, 0) "True" :: [] -(0)-> "A"(0, 0) "True" :: [] -(0)-> "A"(7, 10) "True" :: [] -(0)-> "A"(13, 14) "True" :: [] -(0)-> "A"(14, 2) "True" :: [] -(0)-> "A"(13, 15) "and" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(13, 14) "domatch" :: ["A"(0, 11) x "A"(4, 6) x "A"(0, 0)] -(2)-> "A"(0, 0) "domatch[Ite]" :: ["A"(7, 10) x "A"(0, 11) x "A"(0, 6) x "A"(0, 0)] -(2)-> "A"(0, 0) "eqNatList" :: ["A"(3, 11) x "A"(11, 4)] -(10)-> "A"(0, 0) "eqNatList[Ite]" :: ["A"(13, 14) x "A"(0, 0) x "A"(15, 4) x "A"(0, 0) x "A"(14, 11)] -(11)-> "A"(0, 4) "notEmpty" :: ["A"(4, 0)] -(1)-> "A"(0, 0) "prefix" :: ["A"(0, 0) x "A"(1, 0)] -(1)-> "A"(13, 14) "strmatch" :: ["A"(5, 15) x "A"(15, 14)] -(16)-> "A"(0, 0) Cost Free Signatures: --------------------- "!EQ" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "!EQ" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(6, 8) "!EQ" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 14) "!EQ" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(2)-> "A"_cf(0, 0) "0" :: [] -(0)-> "A"_cf(0, 0) "Cons" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "Cons" :: ["A"_cf(0, 0) x "A"_cf(12, 12)] -(0)-> "A"_cf(0, 12) "Cons" :: ["A"_cf(2, 0) x "A"_cf(2, 0)] -(2)-> "A"_cf(2, 0) "Cons" :: ["A"_cf(1, 0) x "A"_cf(11, 10)] -(1)-> "A"_cf(1, 10) "Cons" :: ["A"_cf(11, 0) x "A"_cf(11, 0)] -(11)-> "A"_cf(11, 0) "Cons" :: ["A"_cf(4, 0) x "A"_cf(4, 0)] -(4)-> "A"_cf(4, 0) "False" :: [] -(0)-> "A"_cf(0, 0) "False" :: [] -(0)-> "A"_cf(0, 4) "False" :: [] -(0)-> "A"_cf(9, 15) "False" :: [] -(0)-> "A"_cf(8, 14) "False" :: [] -(0)-> "A"_cf(14, 14) "False" :: [] -(0)-> "A"_cf(6, 8) "False" :: [] -(0)-> "A"_cf(8, 8) "False" :: [] -(0)-> "A"_cf(0, 8) "False" :: [] -(0)-> "A"_cf(10, 14) "False" :: [] -(0)-> "A"_cf(14, 9) "False" :: [] -(0)-> "A"_cf(14, 8) "False" :: [] -(0)-> "A"_cf(15, 15) "False" :: [] -(0)-> "A"_cf(14, 10) "False" :: [] -(0)-> "A"_cf(14, 15) "False" :: [] -(0)-> "A"_cf(10, 0) "False" :: [] -(0)-> "A"_cf(14, 1) "False" :: [] -(0)-> "A"_cf(0, 15) "False" :: [] -(0)-> "A"_cf(0, 10) "Nil" :: [] -(0)-> "A"_cf(0, 0) "Nil" :: [] -(0)-> "A"_cf(8, 0) "Nil" :: [] -(0)-> "A"_cf(8, 1) "Nil" :: [] -(0)-> "A"_cf(12, 12) "Nil" :: [] -(0)-> "A"_cf(4, 0) "Nil" :: [] -(0)-> "A"_cf(10, 0) "Nil" :: [] -(0)-> "A"_cf(14, 14) "Nil" :: [] -(0)-> "A"_cf(12, 0) "Nil" :: [] -(0)-> "A"_cf(2, 0) "Nil" :: [] -(0)-> "A"_cf(6, 15) "Nil" :: [] -(0)-> "A"_cf(2, 14) "Nil" :: [] -(0)-> "A"_cf(14, 2) "Nil" :: [] -(0)-> "A"_cf(7, 11) "Nil" :: [] -(0)-> "A"_cf(15, 12) "Nil" :: [] -(0)-> "A"_cf(11, 0) "S" :: ["A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "True" :: [] -(0)-> "A"_cf(0, 0) "True" :: [] -(0)-> "A"_cf(0, 4) "True" :: [] -(0)-> "A"_cf(9, 15) "True" :: [] -(0)-> "A"_cf(14, 8) "True" :: [] -(0)-> "A"_cf(0, 8) "True" :: [] -(0)-> "A"_cf(14, 14) "True" :: [] -(0)-> "A"_cf(6, 14) "True" :: [] -(0)-> "A"_cf(10, 14) "True" :: [] -(0)-> "A"_cf(8, 8) "and" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "and" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(8, 14) "and" :: ["A"_cf(0, 8) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 4) "domatch" :: ["A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "domatch" :: ["A"_cf(0, 0) x "A"_cf(2, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "domatch[Ite]" :: ["A"_cf(0, 4) x "A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "domatch[Ite]" :: ["A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "domatch[Ite]" :: ["A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(2, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "eqNatList" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(14, 10) "eqNatList" :: ["A"_cf(11, 0) x "A"_cf(4, 0)] -(1)-> "A"_cf(0, 4) "eqNatList[Ite]" :: ["A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(14, 10) "eqNatList[Ite]" :: ["A"_cf(0, 0) x "A"_cf(0, 0) x "A"_cf(4, 0) x "A"_cf(2, 0) x "A"_cf(11, 0)] -(3)-> "A"_cf(0, 4) "prefix" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 0) "prefix" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(8, 8) "prefix" :: ["A"_cf(0, 0) x "A"_cf(0, 0)] -(0)-> "A"_cf(0, 4) Base Constructors: ------------------ "\"0\"_A" :: [] -(0)-> "A"(1, 0) "\"0\"_A" :: [] -(0)-> "A"(0, 1) "\"Cons\"_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "\"Cons\"_A" :: ["A"(0, 0) x "A"(1, 1)] -(0)-> "A"(0, 1) "\"False\"_A" :: [] -(0)-> "A"(1, 0) "\"False\"_A" :: [] -(0)-> "A"(0, 1) "\"Nil\"_A" :: [] -(0)-> "A"(1, 0) "\"Nil\"_A" :: [] -(0)-> "A"(0, 1) "\"S\"_A" :: ["A"(1, 0)] -(0)-> "A"(1, 0) "\"S\"_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "\"True\"_A" :: [] -(0)-> "A"(1, 0) "\"True\"_A" :: [] -(0)-> "A"(0, 1)